Prooftree is a program for proof-tree visualization during interactive proof development in a theorem prover. It is currently being developed for Coq and Proof General. Prooftree helps against getting lost between different subgoals in interactive proof development. It clearly shows where the current subgoal comes from and thus helps in developing the right plan for solving it.
Prooftree uses different colors for the already proven subgoals, the current branch in the proof and the still open subgoals. Sequent texts are not displayed in the proof tree itself, but they are shown as a tool-tip when the mouse rests over a sequent symbol. Long proof commands are abbreviated in the tree display, but show up in full length as tool-tip. Both, sequents and proof commands, can be shown in the display below the tree (on single click) or in a separate window (on double or shift-click).
Prooftree can mark the proof command that introduced a certain existential variable and thus help to locate the problem when Coq says No more subgoals but non-instantiated existential variables.
Currently, prooftree does only work for Coq proofs. Adding support for a different proof assistant should not be too hard, see the Proof General Adapting manual. Please drop me a line, if you would like to help with another proof assistant.
For older items visit the list of all changes.
Prooftree requires Proof General >= 4.6 or a development version from February 23, 2024. Additionally, Coq version 8.11 or greater is required.
Sources: [prooftree-0.14.tar.gz]
Versions before 0.8 required patched versions of Proof General and Coq and were therefore distributed as a bundle of Prooftree, Proof General and the Coq patches.
Previous versions: 0.13, 0.12, 0.11, 0.10, 0.9, 0.8, 2011-11-01, 2011-10-04, 2011-08-11, 2011-06-14, 2011-04-21, 2011-04-20, 2011-04-18.
Prooftree is implemented in OCaml and Gtk (using version 2.20) with the LablGtk2 bindings. For compilation you therefore need OCaml, Gtk and LablGtk installed. For Debian the packages ocaml-nox and liblablgtk2-ocaml-dev suffice (but the package ocaml-native-compilers is strongly recommended for binary compilation). For Proof General you need Emacs version 26.3.
The communication protocol between Prooftree and Proof General changes now and then. Therefore, only certain versions of Prooftree and Proof General are compatible with each other, see the following table.
| Prooftree version | Proof General version | communication protocol |
|---|---|---|
| 0.14 - latest | >= 4.6 | version 4 |
| 0.11 - 0.13 | >= 4.3pre130327 | version 3 |
| 0.9, 0.10 | 4.2; 4.2pre120110 - 4.3pre130111 | version 2 |
| 0.8 | 4.2pre120104 | version 1 |
Proof-tree display is initially off. To display a proof tree
hit the proof tree icon 
in the toolbar or select the menu entry Proof-General ->
Start/Stop Prooftree or type C-c C-d. If you are
inside a proof, Proof General will immediately display a window
with the proof tree of the current proof. Otherwise it will
remember to start the proof-tree display for the next proof.
Displaying the proof tree of an already started proof requires to retract and redo all proof steps done so far. This should be almost unnoticeable, except for the time it takes.
For comprehensive documentation see the Prooftree help window or the Prooftree man page.
The Proof General Users Manual contains a section about Prooftree with the most essential information. Information about supporting a new proof assistant is contained in the Proof General Adapting Manual.
Prooftree is controlled by Proof General and thus an Emacs subprocess. Proof General does a light analysis of the output of the proof assistant and sends appropriate commands to prooftree. To avoid synchronization trouble, the communication between Proof General and prooftree is (almost) one way: Proof General sends display commands to Prooftree and Prooftree never requests anything from Proof General. To achieve this, Proof General maintains some state for prooftree. For instance, Proof General keeps a mapping of existential variables to goals in which they occur. This mapping helps to decide which goals must be updated inside prooftree when some existential variable gets instantiated.
Drawing a proof tree is just a matter of digging up the right functions for drawing circles and lines inside a drawing area. For Coq proof trees it is, however, a bit more complicated than that.
Coq (and probably other proof assistants as well) displays open goals without any information about their origin. To build a proper proof tree one therefore has to find some other means to decide which goals have been created by the preceding proof command. Therefore, Coq version 8.4 prints unique identification numbers for each goal.
Prooftree is more or less a reimplementation of the graphical proof display of Pvs. The Pvs version is implemented in Tcl/Tk and controlled directly by the Pvs prover process. Therefore, for Pvs, one can start the proof display in the middle of a proof, without the need of rerunning the proof. The Pvs proof display has some performance problems for very large proofs. For a comparison, see this screen shot.
